Runtime Complexity (innermost) proof of /tmp/tmpMPFGSq/10.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 18 ms)

↳2 CdtProblem

↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtUsableRulesProof (⇔, 0 ms)

↳8 CdtProblem

↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳10 CdtProblem

↳11 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳12 CdtProblem

↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 26 ms)

↳14 CdtProblem

↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳16 CdtProblem

↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳18 CdtProblem

↳19 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳20 CdtProblem

↳21 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳22 CdtProblem

↳23 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 48 ms)

↳24 CdtProblem

↳25 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳26 CdtProblem

↳27 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳28 CdtProblem

↳29 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳30 CdtProblem

↳31 CdtUsableRulesProof (⇔, 0 ms)

↳32 CdtProblem

↳33 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 28 ms)

↳34 CdtProblem

↳35 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳36 CdtProblem

↳37 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 14 ms)

↳38 CdtProblem

↳39 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳40 CdtProblem

↳41 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳42 CdtProblem

↳43 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳44 CdtProblem

↳45 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳46 CdtProblem

↳47 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳48 CdtProblem

↳49 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 17 ms)

↳50 CdtProblem

↳51 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 4207 ms)

↳52 CdtProblem

↳53 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳54 CdtProblem

↳55 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳56 CdtProblem

↳57 CdtUsableRulesProof (⇔, 0 ms)

↳58 CdtProblem

↳59 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 2 ms)

↳60 CdtProblem

↳61 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳62 CdtProblem

↳63 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳64 CdtProblem

↳65 CdtUsableRulesProof (⇔, 0 ms)

↳66 CdtProblem

↳67 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 9 ms)

↳68 CdtProblem

↳69 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 17 ms)

↳70 CdtProblem

↳71 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 441 ms)

↳72 CdtProblem

↳73 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳74 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0) → cond2(even(z0), z0)
cond2(true, z0) → cond1(neq(z0, 0), div2(z0))
cond2(false, z0) → cond1(neq(z0, 0), p(z0))
neq(0, 0) → false
neq(0, s(z0)) → true
neq(s(z0), 0) → true
neq(s(z0), s(y)) → neq(z0, y)
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), NEQ(z0, 0), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)), NEQ(z0, 0), P(z0))
NEQ(0, 0) → c3
NEQ(0, s(z0)) → c4
NEQ(s(z0), 0) → c5
NEQ(s(z0), s(y)) → c6(NEQ(z0, y))
EVEN(0) → c7
EVEN(s(0)) → c8
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(0) → c10
DIV2(s(0)) → c11
DIV2(s(s(z0))) → c12(DIV2(z0))
P(0) → c13
P(s(z0)) → c14

S tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), NEQ(z0, 0), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)), NEQ(z0, 0), P(z0))
NEQ(0, 0) → c3
NEQ(0, s(z0)) → c4
NEQ(s(z0), 0) → c5
NEQ(s(z0), s(y)) → c6(NEQ(z0, y))
EVEN(0) → c7
EVEN(s(0)) → c8
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(0) → c10
DIV2(s(0)) → c11
DIV2(s(s(z0))) → c12(DIV2(z0))
P(0) → c13
P(s(z0)) → c14

K tuples:none
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

COND1, COND2, NEQ, EVEN, DIV2, P

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 10 trailing nodes:

NEQ(0, s(z0)) → c4
EVEN(s(0)) → c8
NEQ(0, 0) → c3
EVEN(0) → c7
P(s(z0)) → c14
DIV2(s(0)) → c11
DIV2(0) → c10
NEQ(s(z0), s(y)) → c6(NEQ(z0, y))
P(0) → c13
NEQ(s(z0), 0) → c5

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0) → cond2(even(z0), z0)
cond2(true, z0) → cond1(neq(z0, 0), div2(z0))
cond2(false, z0) → cond1(neq(z0, 0), p(z0))
neq(0, 0) → false
neq(0, s(z0)) → true
neq(s(z0), 0) → true
neq(s(z0), s(y)) → neq(z0, y)
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), NEQ(z0, 0), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)), NEQ(z0, 0), P(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))

S tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), NEQ(z0, 0), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)), NEQ(z0, 0), P(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))

K tuples:none
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

COND1, COND2, EVEN, DIV2

Compound Symbols:

c, c1, c2, c9, c12

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0) → cond2(even(z0), z0)
cond2(true, z0) → cond1(neq(z0, 0), div2(z0))
cond2(false, z0) → cond1(neq(z0, 0), p(z0))
neq(0, 0) → false
neq(0, s(z0)) → true
neq(s(z0), 0) → true
neq(s(z0), s(y)) → neq(z0, y)
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))

S tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))

K tuples:none
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

COND1, EVEN, DIV2, COND2

Compound Symbols:

c, c9, c12, c1, c2

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

cond1(true, z0) → cond2(even(z0), z0)
cond2(true, z0) → cond1(neq(z0, 0), div2(z0))
cond2(false, z0) → cond1(neq(z0, 0), p(z0))
neq(0, s(z0)) → true
neq(s(z0), s(y)) → neq(z0, y)

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))

S tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))

K tuples:none
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

COND1, EVEN, DIV2, COND2

Compound Symbols:

c, c9, c12, c1, c2

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0)) by

COND1(true, 0) → c(COND2(true, 0), EVEN(0))
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, 0) → c(COND2(true, 0), EVEN(0))
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, 0) → c(COND2(true, 0), EVEN(0))
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))

K tuples:none
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c

(11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))

K tuples:none
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c, c

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND1(true, 0) → c(COND2(true, 0))

We considered the (Usable) Rules:

neq(s(z0), 0) → true
neq(0, 0) → false

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x₁, x₂)) = x₁
POL(COND2(x₁, x₂)) = x₂
POL(DIV2(x₁)) = 0
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = 0
POL(even(x₁)) = 0
POL(false) = 0
POL(neq(x₁, x₂)) = x₁
POL(p(x₁)) = 0
POL(s(x₁)) = [1]
POL(true) = [1]

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))

K tuples:

COND1(true, 0) → c(COND2(true, 0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c, c

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0)) by

COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))

K tuples:

COND1(true, 0) → c(COND2(true, 0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))

K tuples:

COND1(true, 0) → c(COND2(true, 0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1

(19) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))

K tuples:

COND1(true, 0) → c(COND2(true, 0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1, c1

(21) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, 0) → c(COND2(true, 0))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1, c1

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))

We considered the (Usable) Rules:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
div2(s(0)) → 0

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]
POL(COND1(x₁, x₂)) = x₂
POL(COND2(x₁, x₂)) = x₂
POL(DIV2(x₁)) = 0
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = x₁
POL(even(x₁)) = [2] + x₁
POL(false) = 0
POL(neq(x₁, x₂)) = 0
POL(p(x₁)) = x₁
POL(s(x₁)) = [1] + x₁
POL(true) = 0

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1, c1

(25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0))) by

COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, 0) → c2(COND1(false, p(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, 0) → c2(COND1(false, p(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, 0) → c2(COND1(false, p(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

(27) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

COND2(false, 0) → c2(COND1(false, p(0)))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

(29) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND1(true, 0) → c(COND2(true, 0))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

(31) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

p(0) → 0

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

(33) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))

We considered the (Usable) Rules:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
div2(s(0)) → 0

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(COND1(x₁, x₂)) = x₂
POL(COND2(x₁, x₂)) = x₂
POL(DIV2(x₁)) = 0
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = x₁
POL(even(x₁)) = 0
POL(false) = 0
POL(neq(x₁, x₂)) = 0
POL(p(x₁)) = x₁
POL(s(x₁)) = [1] + x₁
POL(true) = 0

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

(35) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0)))) by

COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c

(37) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

We considered the (Usable) Rules:none
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(COND1(x₁, x₂)) = [1]
POL(COND2(x₁, x₂)) = [1]
POL(DIV2(x₁)) = 0
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = [1] + x₁
POL(even(x₁)) = [1]
POL(false) = 0
POL(neq(x₁, x₂)) = [1] + x₁ + x₂
POL(p(x₁)) = 0
POL(s(x₁)) = [1]
POL(true) = 0

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c

(39) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0)))) by

COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(0)))) → c1(COND1(neq(s(s(s(0))), 0), s(0)), DIV2(s(s(s(0)))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(0)))) → c1(COND1(neq(s(s(s(0))), 0), s(0)), DIV2(s(s(s(0)))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c

(41) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(true, s(s(s(0)))) → c3(DIV2(s(s(s(0)))))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c, c3

(43) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

COND2(true, s(s(s(0)))) → c3(DIV2(s(s(s(0)))))

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c, c3

(45) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) by

COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(true, s(div2(z0))), DIV2(s(s(z0))))

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(true, s(div2(z0))), DIV2(s(s(z0))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

(47) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND2(true, s(s(z0))) → c1(COND1(true, s(div2(z0))), DIV2(s(s(z0))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

(49) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))

We considered the (Usable) Rules:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
div2(s(0)) → 0

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x₁, x₂)) = x₂
POL(COND2(x₁, x₂)) = x₂
POL(DIV2(x₁)) = 0
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = x₁
POL(even(x₁)) = 0
POL(false) = 0
POL(neq(x₁, x₂)) = [1]
POL(p(x₁)) = x₁
POL(s(x₁)) = [1] + x₁
POL(true) = 0

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

(51) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

DIV2(s(s(z0))) → c12(DIV2(z0))

We considered the (Usable) Rules:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
div2(s(0)) → 0

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]
POL(COND1(x₁, x₂)) = [2]x₂ + [2]x₂²
POL(COND2(x₁, x₂)) = [2]x₂ + [2]x₂²
POL(DIV2(x₁)) = [2] + [2]x₁
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = [1] + x₁
POL(even(x₁)) = 0
POL(false) = 0
POL(neq(x₁, x₂)) = x₂ + [2]x₂²
POL(p(x₁)) = x₁
POL(s(x₁)) = [2] + x₁
POL(true) = 0

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

(53) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, 0) → c1(COND1(neq(0, 0), 0)) by

COND2(true, 0) → c1(COND1(false, 0))

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(true, 0) → c1(COND1(false, 0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

(55) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing nodes:

COND1(true, 0) → c(COND2(true, 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, 0) → c1(COND1(false, 0))

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))

Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c2, c, c1, c1, c3

(57) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

neq(0, 0) → false

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

neq(s(z0), 0) → true
p(s(z0)) → z0
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))

Defined Rule Symbols:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c2, c, c1, c1, c3

(59) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))

We considered the (Usable) Rules:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
even(0) → true
p(s(z0)) → z0
even(s(0)) → false
div2(s(0)) → 0
even(s(s(z0))) → even(z0)

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x₁, x₂)) = [1] + x₂
POL(COND2(x₁, x₂)) = x₁ + x₂
POL(DIV2(x₁)) = 0
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = x₁
POL(even(x₁)) = [1]
POL(false) = [1]
POL(neq(x₁, x₂)) = 0
POL(p(x₁)) = x₁
POL(s(x₁)) = [1] + x₁
POL(true) = 0

(60) Obligation:

Complexity Dependency Tuples Problem
Rules:

neq(s(z0), 0) → true
p(s(z0)) → z0
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))

Defined Rule Symbols:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c2, c, c1, c1, c3

(61) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) by

COND2(false, s(z0)) → c2(COND1(true, z0))

(62) Obligation:

Complexity Dependency Tuples Problem
Rules:

neq(s(z0), 0) → true
p(s(z0)) → z0
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))

Defined Rule Symbols:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c2, c, c1, c1, c3

(63) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) by

COND2(false, s(z0)) → c2(COND1(true, z0))

(64) Obligation:

Complexity Dependency Tuples Problem
Rules:

neq(s(z0), 0) → true
p(s(z0)) → z0
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND2(false, s(z0)) → c2(COND1(true, z0))

K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))

Defined Rule Symbols:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

(65) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

p(s(z0)) → z0

(66) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND2(false, s(z0)) → c2(COND1(true, z0))

K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))

Defined Rule Symbols:

even, neq, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

(67) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND2(false, s(z0)) → c2(COND1(true, z0))

We considered the (Usable) Rules:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(COND1(x₁, x₂)) = x₂
POL(COND2(x₁, x₂)) = x₂
POL(DIV2(x₁)) = [1]
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = x₁
POL(even(x₁)) = 0
POL(false) = 0
POL(neq(x₁, x₂)) = 0
POL(s(x₁)) = [1] + x₁
POL(true) = 0

(68) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND2(false, s(z0)) → c2(COND1(true, z0))

Defined Rule Symbols:

even, neq, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

(69) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

We considered the (Usable) Rules:

div2(0) → 0
neq(s(z0), 0) → true
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x₁, x₂)) = x₁ + x₂
POL(COND2(x₁, x₂)) = x₂
POL(DIV2(x₁)) = 0
POL(EVEN(x₁)) = 0
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = x₁
POL(even(x₁)) = 0
POL(false) = 0
POL(neq(x₁, x₂)) = [1]
POL(s(x₁)) = [1] + x₁
POL(true) = [1]

(70) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))

K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND2(false, s(z0)) → c2(COND1(true, z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))

Defined Rule Symbols:

even, neq, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

(71) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EVEN(s(s(z0))) → c9(EVEN(z0))

We considered the (Usable) Rules:

div2(0) → 0
neq(s(z0), 0) → true
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0

And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(COND1(x₁, x₂)) = [2]x₂² + [2]x₁·x₂
POL(COND2(x₁, x₂)) = [2] + [2]x₂²
POL(DIV2(x₁)) = 0
POL(EVEN(x₁)) = [2]x₁
POL(c(x₁)) = x₁
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(div2(x₁)) = x₁
POL(even(x₁)) = 0
POL(false) = 0
POL(neq(x₁, x₂)) = [2]x₂²
POL(s(x₁)) = [1] + x₁
POL(true) = [2]

(72) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))

Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))

S tuples:none
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND2(false, s(z0)) → c2(COND1(true, z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
EVEN(s(s(z0))) → c9(EVEN(z0))

Defined Rule Symbols:

even, neq, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

(73) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtUsableRulesProof (EQUIVALENT transformation)

(8) Obligation:

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(14) Obligation:

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(24) Obligation:

(25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(26) Obligation:

(27) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(28) Obligation:

(29) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(30) Obligation:

(31) CdtUsableRulesProof (EQUIVALENT transformation)

(32) Obligation:

(33) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(34) Obligation:

(35) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(36) Obligation:

(37) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(38) Obligation:

(39) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(40) Obligation:

(41) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

(42) Obligation:

(43) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(44) Obligation:

(45) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(46) Obligation:

(47) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(48) Obligation:

(49) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(50) Obligation:

(51) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(52) Obligation:

(53) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(54) Obligation:

(55) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(56) Obligation:

(57) CdtUsableRulesProof (EQUIVALENT transformation)

(58) Obligation:

(59) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(60) Obligation:

(61) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(62) Obligation:

(63) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(64) Obligation:

(65) CdtUsableRulesProof (EQUIVALENT transformation)

(66) Obligation:

(67) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(68) Obligation:

(69) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(70) Obligation:

(71) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(72) Obligation:

(73) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

(74) BOUNDS(1, 1)